Definitions | b, t T, , Unit, {i..j }, A, x:A. B(x), P & Q, x:A. B(x), P  Q, priority-select(f;g;as), , tl(l), i< j,  b, i j, if b t else f fi, Y, nth_tl(n;as), hd(l), l[i], A B, i j < k, false , Prop, P  Q, False, true , ||as||, P  Q, P Q, Dec(P),  x. t(x), isl(x), list_accum(x,a.f(x;a);y;l), i j, True, {T}, SQType(T),  x,y. t(x;y), T |